STM: append split2

STM: non nil length

STM: length zero

STM: list decomp

STM: nth tl decomp

STM: nth tl decomp eq

STM: firstn decomp

STM: map append sq

STM: list extensionality

STM: map equal

STM: select equal

STM: list decomp reverse

STM: list append singleton ind

STM: cons one one

STM: map length nat

STM: list 2 decomp

STM: append is nil

STM: append nil sq

STM: comb for nth tl wf

STM: comb for ifthenelse wf

STM: band commutes

STM: null append

STM: select cons tl sq2

ABS: mklist(n;f)

STM: mklist wf

STM: mklist length

STM: mklist select

ABS: (x  l)

STM: l member wf

STM: member exists

STM: map equal2

STM: trivial map

STM: comb for l member wf

STM: member tl

STM: nil member

STM: null member

STM: member null

STM: cons member

STM: l member decidable

STM: member append

STM: select member

STM: member singleton

STM: member map

STM: l member non nil

ABS: agree_on_common(T;as;bs)

STM: agree on common wf

STM: agree on common cons

STM: agree on common weakening

STM: agree on common symmetry

STM: agree on common nil

STM: agree on common cons2

ABS: last(L)

STM: last wf

STM: last lemma

STM: last member

STM: last cons

ABS: reverse_select(l;n)

STM: reverse select wf

ABS: (x ! l)

STM: l member! wf

STM: cons member!

STM: nil member!

ABS: L1  L2

STM: sublist wf

STM: sublist transitivity

STM: length sublist

STM: cons sublist nil

STM: proper sublist length

STM: sublist antisymmetry

STM: nil sublist

STM: cons sublist cons

STM: member sublist

STM: sublist append

STM: comb for sublist wf

STM: sublist weakening

STM: sublist nil

STM: sublist tl

STM: sublist tl2

STM: sublist append front

STM: sublist pair

STM: member iff sublist

ABS: x before y  l

STM: l before wf

STM: weak l before append front

STM: l before append front

STM: l tricotomy

STM: l before member

STM: singleton before

STM: nil before

STM: l before append

STM: l before member2

STM: l before sublist

STM: cons before

STM: before last

STM: l before select

ABS: x << y  l

STM: strong before wf

ABS: same_order(x1;y1;x2;y2;L;T)

STM: same order wf

ABS: y = succ(x) in l P(y)

STM: l succ wf

STM: comb for l succ wf

STM: cons succ

ABS: A List

STM: listp wf

STM: listp properties

STM: hd wf listp

STM: comb for hd wf listp

STM: map equal3

STM: hd map

STM: map wf listp

STM: cons wf listp

STM: comb for cons wf listp

ABS: count(P;L)

STM: count wf

ABS: filter(P;l)

STM: filter wf

STM: filter sublist

STM: filter is sublist

STM: length filter

STM: member filter

STM: filter before

STM: agree on common filter

STM: filter functionality

STM: filter append

STM: filter filter

STM: filter filter reduce

STM: filter type

STM: filter map

ABS: l1  l2

STM: iseg wf

STM: cons iseg

STM: iseg transitivity

STM: iseg append

STM: iseg extend

STM: firstn is iseg

STM: iseg transitivity2

STM: comb for iseg wf

STM: iseg weakening

STM: nil iseg

STM: iseg select

STM: iseg member

STM: iseg nil

STM: agree on common iseg

STM: filter iseg

STM: iseg filter

STM: iseg append0

STM: iseg length

STM: iseg is sublist

ABS: l1 || l2

STM: compat wf

STM: common iseg compat

ABS: list_accum(x,a.f(x;a);y;l)

STM: list accum wf

STM: comb for list accum wf

STM: list accum split

ABS: zip(as;bs)

STM: zip wf

STM: zip length

STM: select zip

STM: length zip

ABS: unzip(as)

STM: unzip wf

STM: unzip zip

STM: zip unzip

ABS: first x  as s.t. P(x) else d

STM: find wf

STM: find property

ABS: list_all(x.P(x);l)

STM: list all wf

STM: list all iff

ABS: no_repeats(T;l)

STM: no repeats wf

STM: no repeats iff

STM: no repeats cons

STM: append overlapping sublists

STM: l before transitivity

STM: l before antisymmetry

STM: no repeats nil

ABS: l_disjoint(T;l1;l2)

STM: l disjoint wf

STM: l disjoint member

STM: no repeats append

ABS: append_rel(T;L1;L2;L)

STM: append rel wf

ABS: safety(A;tr.P(tr))

STM: safety wf

STM: no repeats safety

STM: filter safety

STM: all safety

STM: safety and

STM: safety nil

STM: cond safety and

ABS: xL. P(x)

STM: l all wf

STM: l all append

STM: l all filter

STM: comb for l all wf

STM: l all cons

STM: agree on common append

STM: filter trivial

STM: filter trivial2

STM: filter is nil

STM: filter is singleton

STM: list set type

STM: l all fwd

STM: l all map

STM: l all nil

STM: l all reduce

STM: split rel last

STM: sublist filter

STM: sublist filter set type

STM: l before filter set type

STM: l before filter

STM: no repeats filter

STM: decidable l all

STM: filter is empty

STM: filter is singleton2

STM: append split

ABS: (x<yL.P(x;y))

STM: l all2 wf

STM: l all2 cons

ABS: (xaL.P(x))

STM: l all since wf

ABS: (xL.P(x))

STM: l exists wf

STM: l exists append

STM: l exists nil

STM: l exists cons

STM: l exists reduce

STM: decidable l exists

ABS: mapfilter(f;P;L)

STM: mapfilter wf

STM: member map filter

ABS: split_tail(L | x.f(x))

STM: split tail wf

STM: split tail trivial

STM: split tail max

STM: split tail correct

STM: split tail rel

STM: split tail lemma

ABS: reduce2(f;k;i;as)

STM: reduce2 wf

STM: reduce2 shift

STM: comb for reduce2 wf

ABS: filter2(P;L)

STM: filter2 wf

STM: cons filter2

STM: filter filter2

STM: member filter2

STM: filter2 functionality

STM: filter of filter2

ABS: sublist_occurence(T;L1;L2;f)

STM: sublist occurence wf

STM: range sublist

ABS: disjoint_sublists(T;L1;L2;L)

STM: disjoint sublists wf

STM: disjoint sublists sublist

STM: disjoint sublists witness

STM: length disjoint sublists

ABS: interleaving(T;L1;L2;L)

STM: interleaving wf

STM: l before interleaving

STM: nil interleaving

STM: nil interleaving2

STM: member interleaving

STM: cons interleaving

STM: comb for interleaving wf

STM: length interleaving

STM: interleaving of nil

STM: interleaving symmetry

STM: cons interleaving2

STM: interleaving of cons

STM: interleaving filter2

STM: filter interleaving

STM: interleaving as filter

STM: interleaving as filter 2

STM: sublist interleaved

STM: interleaved split

STM: interleaving sublist

STM: append interleaving

STM: sublist append1

STM: sublist iseg

STM: l before iseg

ABS: interleaving_occurence(T;L1;L2;L;f1;f2)

STM: interleaving occurence wf

STM: interleaving implies occurence

STM: interleaving occurence onto

STM: interleaving split

STM: interleaving singleton

STM: last with property

STM: occurence implies interleaving

STM: filter is interleaving

STM: filter interleaving occurence

ABS: causal_order(L;R;P;Q)

STM: causal order wf

STM: causal order filter iseg

STM: causal order transitivity

STM: causal order reflexive

STM: causal order or

STM: causal order sigma

STM: causal order monotonic

STM: causal order monotonic2

STM: causal order monotonic3

STM: causal order monotonic4

ABS: interleaved_family_occurence(T;I;L;L2;f)

STM: interleaved family occurence wf

ABS: interleaved_family(T;I;L;L2)

STM: interleaved family wf

ABS: (L o f)

STM: permute list wf

STM: permute list select

STM: permute list length

STM: permute permute list

ABS: swap(L;i;j)

STM: swap wf

STM: swap select

STM: swap length

STM: swap swap

STM: swapped select

STM: swap cons

STM: swap adjacent decomp

STM: l before swap

STM: map swap

STM: comb for swap wf

ABS: guarded_permutation(T;P)

STM: guarded permutation wf

STM: guarded permutation transitivity

ABS: count(i<j<||L|| : P L i j)

STM: count index pairs wf

ABS: count(x < y in L | P(x;y))

STM: count pairs wf

ABS: index-of-first x in L.P(x)

STM: first index wf

STM: first index cons

ABS: agree_on(T;x.P(x))

STM: agree on wf

STM: first index equal

STM: iseg map

STM: safety induced

STM: agree on equiv

ABS: strong_safety(T;tr.P(tr))

STM: strong safety wf

STM: filter strong safety

STM: strong safety safety

ABS: l_subset(T;as;bs)

STM: l subset wf

ABS: sublist*(T;as;bs)

STM: sublist* wf

STM: sublist* filter

DIR: aux